Existing protocol verifiers work on ad-hoc, hand-written, abstract descriptions of security protocols. The gap between the hand-written description and the running code can lead to errors. To make matters worse, to check and to maintain the hand written description is substantially labor intensive and time consuming.